<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>SemOpt: src/Preferred.cpp Source File</title>

<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
<link href="navtree.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="resize.js"></script>
<script type="text/javascript" src="navtree.js"></script>
<script type="text/javascript">
  $(document).ready(initResizable);
</script>


</head>
<body>
<div id="top"><!-- do not remove this div! -->


<div id="titlearea">
<table cellspacing="0" cellpadding="0">
 <tbody>
 <tr style="height: 56px;">
  
  
  <td style="padding-left: 0.5em;">
   <div id="projectname">SemOpt
   &#160;<span id="projectnumber">0.2alpha5-SCC</span>
   </div>
   
  </td>
  
  
  
 </tr>
 </tbody>
</table>
</div>

<!-- Generated by Doxygen 1.7.6.1 -->
  <div id="navrow1" class="tabs">
    <ul class="tablist">
      <li><a href="index.html"><span>Main&#160;Page</span></a></li>
      <li><a href="annotated.html"><span>Classes</span></a></li>
      <li class="current"><a href="files.html"><span>Files</span></a></li>
    </ul>
  </div>
  <div id="navrow2" class="tabs2">
    <ul class="tablist">
      <li><a href="files.html"><span>File&#160;List</span></a></li>
      <li><a href="globals.html"><span>File&#160;Members</span></a></li>
    </ul>
  </div>
</div>
<div id="side-nav" class="ui-resizable side-nav-resizable">
  <div id="nav-tree">
    <div id="nav-tree-contents">
    </div>
  </div>
  <div id="splitbar" style="-moz-user-select:none;" 
       class="ui-resizable-handle">
  </div>
</div>
<script type="text/javascript">
  initNavTree('Preferred_8cpp.html','');
</script>
<div id="doc-content">
<div class="header">
  <div class="headertitle">
<div class="title">src/Preferred.cpp</div>  </div>
</div><!--header-->
<div class="contents">
<div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*</span>
<a name="l00002"></a>00002 <span class="comment"> * Preferred.cpp</span>
<a name="l00003"></a>00003 <span class="comment"> *</span>
<a name="l00004"></a>00004 <span class="comment"> *  Created on: 10 Jun 2013</span>
<a name="l00005"></a>00005 <span class="comment"> *      Author: geryo</span>
<a name="l00006"></a>00006 <span class="comment"> */</span>
<a name="l00007"></a>00007 
<a name="l00008"></a>00008 <span class="preprocessor">#include &quot;<a class="code" href="Preferred_8h.html" title="use this class to compute PrefSAT">Preferred.h</a>&quot;</span>
<a name="l00009"></a>00009 
<a name="l00024"></a>00024 <span class="keywordtype">void</span> Preferred::cleanlabs()
<a name="l00025"></a>00025 {
<a name="l00026"></a>00026         <span class="keywordflow">while</span> (!this-&gt;labellings.empty())
<a name="l00027"></a>00027                 this-&gt;labellings.pop_back();
<a name="l00028"></a>00028 }
<a name="l00029"></a>00029 
<a name="l00033"></a>00033 <span class="keywordtype">int</span> Preferred::compute_new_pigreek()
<a name="l00034"></a>00034 {
<a name="l00035"></a>00035         <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a> subtraction = <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a>();
<a name="l00036"></a>00036         this-&gt;A-&gt;setminus(this-&gt;C, &amp;subtraction);
<a name="l00037"></a>00037 
<a name="l00038"></a>00038         <span class="keywordflow">for</span> (<a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> it_sub = subtraction.<a class="code" href="classSetArguments.html#aaee058feaed861edf27739fa04f374ef" title="Begin of the iterator for this set of arguments.">begin</a>();
<a name="l00039"></a>00039                         it_sub != subtraction.<a class="code" href="classSetArguments.html#a551272d71c803f64efc155b04f41e775" title="End of the iterator for this set of arguments.">end</a>(); it_sub++)
<a name="l00040"></a>00040         {
<a name="l00041"></a>00041                 <span class="keywordflow">if</span> (debug)
<a name="l00042"></a>00042                 {
<a name="l00043"></a>00043                         cout &lt;&lt; <span class="stringliteral">&quot;Subtraction &quot;</span> &lt;&lt; (*it_sub)-&gt;getName() &lt;&lt; endl;
<a name="l00044"></a>00044                 }
<a name="l00045"></a>00045                 <span class="comment">//c2</span>
<a name="l00046"></a>00046                 this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00047"></a>00047                                 <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(1, (*it_sub)-&gt;NotInVar()));
<a name="l00048"></a>00048                 this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00049"></a>00049                                 <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(2, (*it_sub)-&gt;OutVar(), (*it_sub)-&gt;UndecVar()));
<a name="l00050"></a>00050                 this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00051"></a>00051                                 <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(2, (*it_sub)-&gt;NotOutVar(), (*it_sub)-&gt;NotUndecVar()));
<a name="l00052"></a>00052 
<a name="l00053"></a>00053                 <span class="comment">//c-to-add</span>
<a name="l00054"></a>00054                 <span class="keywordflow">if</span> ((*it_sub)-&gt;get_attackers()-&gt;empty())
<a name="l00055"></a>00055                 {
<a name="l00056"></a>00056                         this-&gt;sat_new_pigreek.appendOrClause(<a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(1, (*it_sub)-&gt;UndecVar()));
<a name="l00057"></a>00057                 }
<a name="l00058"></a>00058 
<a name="l00059"></a>00059         }
<a name="l00060"></a>00060 
<a name="l00061"></a>00061         <span class="keywordflow">if</span> (debug)
<a name="l00062"></a>00062         {
<a name="l00063"></a>00063                 cout &lt;&lt; <span class="stringliteral">&quot;Set arguments: &quot;</span> &lt;&lt; endl;
<a name="l00064"></a>00064                 cout &lt;&lt; *(this-&gt;A) &lt;&lt; endl;
<a name="l00065"></a>00065 
<a name="l00066"></a>00066                 cout &lt;&lt; <span class="stringliteral">&quot;C set:&quot;</span> &lt;&lt; endl;
<a name="l00067"></a>00067                 cout &lt;&lt; *(this-&gt;C) &lt;&lt; endl;
<a name="l00068"></a>00068         }
<a name="l00069"></a>00069 
<a name="l00070"></a>00070         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a> noempty_clause = <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>();
<a name="l00071"></a>00071         <span class="keywordflow">for</span> (<a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> it_args = this-&gt;C-&gt;begin();
<a name="l00072"></a>00072                         it_args != this-&gt;C-&gt;end(); it_args++)
<a name="l00073"></a>00073         {
<a name="l00074"></a>00074                 <span class="comment">//c1</span>
<a name="l00075"></a>00075                 <span class="keywordflow">if</span> (encoding == 0 || encoding == 1 || encoding == 2 || encoding == 3
<a name="l00076"></a>00076                                 || encoding == 4 || encoding == 5)
<a name="l00077"></a>00077                 {
<a name="l00078"></a>00078                         this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00079"></a>00079                                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(3, (*it_args)-&gt;InVar(), (*it_args)-&gt;OutVar(),
<a name="l00080"></a>00080                                                         (*it_args)-&gt;UndecVar()));
<a name="l00081"></a>00081 
<a name="l00082"></a>00082                         this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00083"></a>00083                                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(2, (*it_args)-&gt;NotInVar(),
<a name="l00084"></a>00084                                                         (*it_args)-&gt;NotOutVar()));
<a name="l00085"></a>00085 
<a name="l00086"></a>00086                         this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00087"></a>00087                                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(2, (*it_args)-&gt;NotInVar(),
<a name="l00088"></a>00088                                                         (*it_args)-&gt;NotUndecVar()));
<a name="l00089"></a>00089 
<a name="l00090"></a>00090                         this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00091"></a>00091                                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(2, (*it_args)-&gt;NotOutVar(),
<a name="l00092"></a>00092                                                         (*it_args)-&gt;NotUndecVar()));
<a name="l00093"></a>00093                 }
<a name="l00094"></a>00094 
<a name="l00095"></a>00095                 noempty_clause.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*it_args)-&gt;InVar());
<a name="l00096"></a>00096 
<a name="l00097"></a>00097                 <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a> *pred = (*it_args)-&gt;get_attackers();
<a name="l00098"></a>00098 
<a name="l00099"></a>00099                 <span class="keywordflow">if</span> (debug)
<a name="l00100"></a>00100                 {
<a name="l00101"></a>00101                         cout &lt;&lt; <span class="stringliteral">&quot;predecessors of &quot;</span> &lt;&lt; (*it_args)-&gt;getName() &lt;&lt; <span class="stringliteral">&quot;: &quot;</span>;
<a name="l00102"></a>00102 
<a name="l00103"></a>00103                         <span class="keywordflow">for</span> (<a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> it_pred = pred-&gt;<a class="code" href="classSetArguments.html#aaee058feaed861edf27739fa04f374ef" title="Begin of the iterator for this set of arguments.">begin</a>();
<a name="l00104"></a>00104                                         it_pred != pred-&gt;<a class="code" href="classSetArguments.html#a551272d71c803f64efc155b04f41e775" title="End of the iterator for this set of arguments.">end</a>(); it_pred++)
<a name="l00105"></a>00105                                 cout &lt;&lt; (*it_pred)-&gt;getName() &lt;&lt; <span class="stringliteral">&quot; &quot;</span>;
<a name="l00106"></a>00106                         cout &lt;&lt; endl;
<a name="l00107"></a>00107                 }
<a name="l00108"></a>00108 
<a name="l00109"></a>00109                 <span class="keywordflow">if</span> (pred-&gt;<a class="code" href="classSetArguments.html#a91e548daa6d0859946c8604b1ebb8c5a" title="Check wether or not this set is empty.">empty</a>())
<a name="l00110"></a>00110                 {
<a name="l00111"></a>00111                         <span class="comment">//c3</span>
<a name="l00112"></a>00112                         this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00113"></a>00113                                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(1, (*it_args)-&gt;InVar()));
<a name="l00114"></a>00114 
<a name="l00115"></a>00115                         this-&gt;sat_new_pigreek.appendOrClause((*it_args)-&gt;NotOutVar());
<a name="l00116"></a>00116 
<a name="l00117"></a>00117                         this-&gt;sat_new_pigreek.appendOrClause((*it_args)-&gt;NotUndecVar());
<a name="l00118"></a>00118                 }
<a name="l00119"></a>00119                 <span class="keywordflow">else</span>
<a name="l00120"></a>00120                 {
<a name="l00121"></a>00121                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a> c4_last_clause = <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>();
<a name="l00122"></a>00122                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a> c9_or_undec_clause = <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>();
<a name="l00123"></a>00123                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a> c8_bigor_clause = <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>();
<a name="l00124"></a>00124 
<a name="l00125"></a>00125                         <span class="keywordflow">for</span> (<a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> it_pred = pred-&gt;<a class="code" href="classSetArguments.html#aaee058feaed861edf27739fa04f374ef" title="Begin of the iterator for this set of arguments.">begin</a>();
<a name="l00126"></a>00126                                         it_pred != pred-&gt;<a class="code" href="classSetArguments.html#a551272d71c803f64efc155b04f41e775" title="End of the iterator for this set of arguments.">end</a>(); it_pred++)
<a name="l00127"></a>00127                         {
<a name="l00128"></a>00128 
<a name="l00129"></a>00129                                 <span class="keywordflow">if</span> (!this-&gt;A-&gt;exists(*it_pred))
<a name="l00130"></a>00130                                         <span class="keywordflow">continue</span>;
<a name="l00131"></a>00131 
<a name="l00132"></a>00132                                 <span class="comment">//c5</span>
<a name="l00133"></a>00133                                 <span class="keywordflow">if</span> (encoding == 0 || encoding == 1 || encoding == 3
<a name="l00134"></a>00134                                                 || encoding == 5)
<a name="l00135"></a>00135                                 {
<a name="l00136"></a>00136                                         this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00137"></a>00137                                                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(2, (*it_args)-&gt;NotInVar(),
<a name="l00138"></a>00138                                                                         (*it_pred)-&gt;OutVar()));
<a name="l00139"></a>00139                                 }
<a name="l00140"></a>00140 
<a name="l00141"></a>00141                                 <span class="comment">//c4</span>
<a name="l00142"></a>00142                                 <span class="keywordflow">if</span> (encoding == 0 || encoding == 2 || encoding == 3
<a name="l00143"></a>00143                                                 || encoding == 5)
<a name="l00144"></a>00144                                 {
<a name="l00145"></a>00145                                         c4_last_clause.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*it_pred)-&gt;NotOutVar());
<a name="l00146"></a>00146                                 }
<a name="l00147"></a>00147 
<a name="l00148"></a>00148                                 <span class="comment">//c9</span>
<a name="l00149"></a>00149                                 <span class="keywordflow">if</span> (encoding == 0 || encoding == 1 || encoding == 4
<a name="l00150"></a>00150                                                 || encoding == 5)
<a name="l00151"></a>00151                                 {
<a name="l00152"></a>00152                                         this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00153"></a>00153                                                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(2, (*it_args)-&gt;NotUndecVar(),
<a name="l00154"></a>00154                                                                         (*it_pred)-&gt;NotInVar()));
<a name="l00155"></a>00155 
<a name="l00156"></a>00156                                         c9_or_undec_clause.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*it_pred)-&gt;UndecVar());
<a name="l00157"></a>00157                                 }
<a name="l00158"></a>00158 
<a name="l00159"></a>00159                                 <span class="keywordflow">if</span> (encoding == 0 || encoding == 2 || encoding == 4
<a name="l00160"></a>00160                                                 || encoding == 5)
<a name="l00161"></a>00161                                 {
<a name="l00162"></a>00162                                         c8_bigor_clause.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*it_pred)-&gt;InVar());
<a name="l00163"></a>00163                                 }
<a name="l00164"></a>00164                         }
<a name="l00165"></a>00165 
<a name="l00166"></a>00166                         <span class="comment">//c4-end</span>
<a name="l00167"></a>00167                         <span class="keywordflow">if</span> (encoding == 0 || encoding == 2 || encoding == 3
<a name="l00168"></a>00168                                         || encoding == 5)
<a name="l00169"></a>00169                         {
<a name="l00170"></a>00170                                 c4_last_clause.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*it_args)-&gt;InVar());
<a name="l00171"></a>00171                                 this-&gt;sat_new_pigreek.appendOrClause(c4_last_clause);
<a name="l00172"></a>00172                         }
<a name="l00173"></a>00173 
<a name="l00174"></a>00174                         <span class="comment">//c9-end</span>
<a name="l00175"></a>00175                         <span class="keywordflow">if</span> (encoding == 0 || encoding == 1 || encoding == 4
<a name="l00176"></a>00176                                         || encoding == 5)
<a name="l00177"></a>00177                         {
<a name="l00178"></a>00178                                 c9_or_undec_clause.<a class="code" href="classOrClause.html#a3ad02fa758db9d8b4a432e4c5ee7638e" title="Method for adding a variable at the beginning of the clause.">addHeadVariable</a>((*it_args)-&gt;NotUndecVar());
<a name="l00179"></a>00179                                 this-&gt;sat_new_pigreek.appendOrClause(c9_or_undec_clause);
<a name="l00180"></a>00180                         }
<a name="l00181"></a>00181 
<a name="l00182"></a>00182                         <span class="comment">//c8</span>
<a name="l00183"></a>00183                         <span class="keywordflow">if</span> (encoding == 0 || encoding == 2 || encoding == 4
<a name="l00184"></a>00184                                         || encoding == 5)
<a name="l00185"></a>00185                         {
<a name="l00186"></a>00186                                 <span class="keywordflow">for</span> (<a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> it_pred = pred-&gt;<a class="code" href="classSetArguments.html#aaee058feaed861edf27739fa04f374ef" title="Begin of the iterator for this set of arguments.">begin</a>();
<a name="l00187"></a>00187                                                 it_pred != pred-&gt;<a class="code" href="classSetArguments.html#a551272d71c803f64efc155b04f41e775" title="End of the iterator for this set of arguments.">end</a>(); it_pred++)
<a name="l00188"></a>00188                                 {
<a name="l00189"></a>00189                                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a> to_add = <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>();
<a name="l00190"></a>00190                                         c8_bigor_clause.<a class="code" href="classOrClause.html#ae8edb2f491a3b4f5d8bd402ef1788d82" title="Method for cloning this OrClause into a new OrClause that is passed as input output parameter...">clone</a>(&amp;to_add);
<a name="l00191"></a>00191                                         to_add.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*it_pred)-&gt;NotUndecVar());
<a name="l00192"></a>00192                                         to_add.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*it_args)-&gt;UndecVar());
<a name="l00193"></a>00193                                         this-&gt;sat_new_pigreek.appendOrClause(to_add);
<a name="l00194"></a>00194                                 }
<a name="l00195"></a>00195                         }
<a name="l00196"></a>00196 
<a name="l00197"></a>00197                 }
<a name="l00198"></a>00198         }
<a name="l00199"></a>00199 
<a name="l00200"></a>00200         <span class="keywordflow">for</span> (<a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> it_args = this-&gt;A-&gt;begin();
<a name="l00201"></a>00201                         it_args != this-&gt;A-&gt;end(); it_args++)
<a name="l00202"></a>00202         {
<a name="l00203"></a>00203 
<a name="l00204"></a>00204                 <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a> c7_last_clause = <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>();
<a name="l00205"></a>00205                 <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a> *pred = (*it_args)-&gt;get_attackers();
<a name="l00206"></a>00206 
<a name="l00207"></a>00207                 <span class="keywordflow">if</span> (pred-&gt;<a class="code" href="classSetArguments.html#a91e548daa6d0859946c8604b1ebb8c5a" title="Check wether or not this set is empty.">empty</a>())
<a name="l00208"></a>00208                         <span class="keywordflow">continue</span>;
<a name="l00209"></a>00209 
<a name="l00210"></a>00210                 <span class="keywordflow">for</span> (<a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> it_pred = pred-&gt;<a class="code" href="classSetArguments.html#aaee058feaed861edf27739fa04f374ef" title="Begin of the iterator for this set of arguments.">begin</a>();
<a name="l00211"></a>00211                                 it_pred != pred-&gt;<a class="code" href="classSetArguments.html#a551272d71c803f64efc155b04f41e775" title="End of the iterator for this set of arguments.">end</a>(); it_pred++)
<a name="l00212"></a>00212                 {
<a name="l00213"></a>00213 
<a name="l00214"></a>00214                         <span class="keywordflow">if</span> (!this-&gt;A-&gt;exists(*it_pred))
<a name="l00215"></a>00215                                 <span class="keywordflow">continue</span>;
<a name="l00216"></a>00216 
<a name="l00217"></a>00217                         <span class="comment">//c6</span>
<a name="l00218"></a>00218                         <span class="keywordflow">if</span> (encoding == 0 || encoding == 2 || encoding == 3
<a name="l00219"></a>00219                                         || encoding == 4)
<a name="l00220"></a>00220                         {
<a name="l00221"></a>00221                                 this-&gt;sat_new_pigreek.appendOrClause(
<a name="l00222"></a>00222                                                 <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(2, (*it_pred)-&gt;NotInVar(),
<a name="l00223"></a>00223                                                                 (*it_args)-&gt;OutVar()));
<a name="l00224"></a>00224                         }
<a name="l00225"></a>00225 
<a name="l00226"></a>00226                         <span class="comment">//c7</span>
<a name="l00227"></a>00227                         <span class="keywordflow">if</span> (encoding == 0 || encoding == 1 || encoding == 3
<a name="l00228"></a>00228                                         || encoding == 4)
<a name="l00229"></a>00229                         {
<a name="l00230"></a>00230                                 c7_last_clause.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*it_pred)-&gt;InVar());
<a name="l00231"></a>00231                         }
<a name="l00232"></a>00232                 }
<a name="l00233"></a>00233 
<a name="l00234"></a>00234                 <span class="comment">//c7-end</span>
<a name="l00235"></a>00235                 <span class="keywordflow">if</span> (encoding == 0 || encoding == 1 || encoding == 3 || encoding == 4)
<a name="l00236"></a>00236                 {
<a name="l00237"></a>00237                         c7_last_clause.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*it_args)-&gt;NotOutVar());
<a name="l00238"></a>00238                         this-&gt;sat_new_pigreek.appendOrClause(c7_last_clause);
<a name="l00239"></a>00239                 }
<a name="l00240"></a>00240 
<a name="l00241"></a>00241         }
<a name="l00242"></a>00242 
<a name="l00243"></a>00243         this-&gt;sat_new_pigreek.appendOrClause(noempty_clause);
<a name="l00244"></a>00244 
<a name="l00245"></a>00245         <span class="keywordflow">return</span> this-&gt;sat_new_pigreek.size();
<a name="l00246"></a>00246 }
<a name="l00247"></a>00247 
<a name="l00255"></a>00255 <span class="keywordtype">bool</span> Preferred::satlab(<a class="code" href="classSATFormulae.html" title="Class encompassing a list of `OrClause` linked by and operators.">SATFormulae</a> sat, <a class="code" href="classLabelling.html" title="Class representing a single labelling assignment.">Labelling</a> *lab)
<a name="l00256"></a>00256 {
<a name="l00257"></a>00257         stringstream cnf_string(stringstream::in | stringstream::out);
<a name="l00258"></a>00258         sat.<a class="code" href="classSATFormulae.html#aa2f0f69c190ff01d8ab48e426d89e665" title="Method for transforming the SAT formulae into a string `DIMACS` compliant.">toSS</a>(&amp;cnf_string);
<a name="l00259"></a>00259 
<a name="l00260"></a>00260         <span class="keywordflow">if</span> (debug)
<a name="l00261"></a>00261         {
<a name="l00262"></a>00262                 cout &lt;&lt; <span class="stringliteral">&quot;Preparing the satsolver&quot;</span> &lt;&lt; <span class="stringliteral">&quot;\n&quot;</span>;
<a name="l00263"></a>00263                 cout &lt;&lt; cnf_string.str() &lt;&lt; endl;
<a name="l00264"></a>00264         }
<a name="l00265"></a>00265 
<a name="l00266"></a>00266         vector&lt;int&gt; lastcompfound = vector&lt;int&gt;();
<a name="l00267"></a>00267         <span class="keywordtype">int</span> retsat = precosat_lib(&amp;cnf_string,
<a name="l00268"></a>00268                         3 * ((*(this-&gt;A-&gt;begin()))-&gt;get_af()-&gt;numArgs()), sat.<a class="code" href="classSATFormulae.html#a8f519b3240b275633769ed70c9583d5d" title="Method returning the number of OrClause.">size</a>(),
<a name="l00269"></a>00269                         &amp;lastcompfound);
<a name="l00270"></a>00270 
<a name="l00271"></a>00271         <span class="keywordflow">if</span> (debug)
<a name="l00272"></a>00272         {
<a name="l00273"></a>00273                 cout &lt;&lt; retsat &lt;&lt; endl;
<a name="l00274"></a>00274 
<a name="l00275"></a>00275                 <span class="keywordflow">for</span> (vector&lt;int&gt;::iterator solit = lastcompfound.begin();
<a name="l00276"></a>00276                                 solit != lastcompfound.end(); solit++)
<a name="l00277"></a>00277                 {
<a name="l00278"></a>00278                         cout &lt;&lt; *solit &lt;&lt; <span class="stringliteral">&quot; &quot;</span>;
<a name="l00279"></a>00279                 }
<a name="l00280"></a>00280                 cout &lt;&lt; endl;
<a name="l00281"></a>00281         }
<a name="l00282"></a>00282 
<a name="l00283"></a>00283         <span class="keywordflow">if</span> (retsat != 20)
<a name="l00284"></a>00284         {
<a name="l00285"></a>00285                 <span class="keywordflow">for</span> (<a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> it = this-&gt;A-&gt;begin(); it != this-&gt;A-&gt;end();
<a name="l00286"></a>00286                                 it++)
<a name="l00287"></a>00287                 {
<a name="l00288"></a>00288                         <span class="keywordflow">if</span> (find(lastcompfound.begin(), lastcompfound.end(), (*it)-&gt;InVar())
<a name="l00289"></a>00289                                         != lastcompfound.end())
<a name="l00290"></a>00290                         {
<a name="l00291"></a>00291                                 lab-&gt;<a class="code" href="classLabelling.html#a79e25a77b942e8395431fceceea2bb63" title="Add a new label to this set of labelling.">add_label</a>((*it), <a class="code" href="classLabelling.html#aaf7f367dd2253b297cad3c622a0d2f49" title="Label representing an `in` argument.">Labelling::lab_in</a>);
<a name="l00292"></a>00292                                 <span class="keywordflow">if</span> (debug)
<a name="l00293"></a>00293                                 {
<a name="l00294"></a>00294                                         cout &lt;&lt; (*it)-&gt;getName() &lt;&lt; endl;
<a name="l00295"></a>00295                                 }
<a name="l00296"></a>00296                                 <span class="keywordflow">continue</span>;
<a name="l00297"></a>00297                         }
<a name="l00298"></a>00298                         <span class="keywordflow">if</span> (find(lastcompfound.begin(), lastcompfound.end(),
<a name="l00299"></a>00299                                         (*it)-&gt;OutVar()) != lastcompfound.end())
<a name="l00300"></a>00300                         {
<a name="l00301"></a>00301                                 lab-&gt;<a class="code" href="classLabelling.html#a79e25a77b942e8395431fceceea2bb63" title="Add a new label to this set of labelling.">add_label</a>((*it), <a class="code" href="classLabelling.html#afed946f9be5cb9f3d60ca37e4baf45ba" title="Label representing an `out` argument.">Labelling::lab_out</a>);
<a name="l00302"></a>00302                                 <span class="keywordflow">continue</span>;
<a name="l00303"></a>00303                         }
<a name="l00304"></a>00304                         <span class="keywordflow">if</span> (find(lastcompfound.begin(), lastcompfound.end(),
<a name="l00305"></a>00305                                         (*it)-&gt;UndecVar()) != lastcompfound.end())
<a name="l00306"></a>00306                         {
<a name="l00307"></a>00307                                 lab-&gt;<a class="code" href="classLabelling.html#a79e25a77b942e8395431fceceea2bb63" title="Add a new label to this set of labelling.">add_label</a>((*it), <a class="code" href="classLabelling.html#a4ae2c985855b2a4c084618b6493b0d92" title="Label representing an `undec` argument.">Labelling::lab_undec</a>);
<a name="l00308"></a>00308                                 <span class="keywordflow">continue</span>;
<a name="l00309"></a>00309                         }
<a name="l00310"></a>00310                 }
<a name="l00311"></a>00311                 <span class="keywordflow">if</span> (debug)
<a name="l00312"></a>00312                 {
<a name="l00313"></a>00313                         cout &lt;&lt; endl;
<a name="l00314"></a>00314                         cout &lt;&lt; <span class="stringliteral">&quot;in &quot;</span> &lt;&lt; *(lab-&gt;<a class="code" href="classLabelling.html#af8aa0d976a665c1a9ebbdb801d0a867d" title="Returns the set of arguments labelled as `in`.">inargs</a>()) &lt;&lt; endl;
<a name="l00315"></a>00315                         cout &lt;&lt; <span class="stringliteral">&quot;out &quot;</span> &lt;&lt; *(lab-&gt;<a class="code" href="classLabelling.html#afc828a13d1a3e406f56fa1f212b4824d" title="Returns the set of arguments labelled as `out`.">outargs</a>()) &lt;&lt; endl;
<a name="l00316"></a>00316                         cout &lt;&lt; <span class="stringliteral">&quot;undec &quot;</span> &lt;&lt; *(lab-&gt;<a class="code" href="classLabelling.html#aedf4e3c3b0150317e5350945f088a424" title="Returns the set of arguments labelled as `undec`.">undecargs</a>()) &lt;&lt; endl;
<a name="l00317"></a>00317                 }
<a name="l00318"></a>00318                 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00319"></a>00319         }
<a name="l00320"></a>00320         <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00321"></a>00321 }
<a name="l00322"></a>00322 
<a name="l00323"></a>00323 <span class="keywordtype">void</span> Preferred::prefSAT(<a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a> *the_a, <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a> *the_c)
<a name="l00324"></a>00324 {
<a name="l00325"></a>00325         this-&gt;cleanlabs();
<a name="l00326"></a>00326         this-&gt;A = the_a;
<a name="l00327"></a>00327         this-&gt;C = the_c;
<a name="l00328"></a>00328         this-&gt;compute_new_pigreek();
<a name="l00329"></a>00329         <a class="code" href="classSATFormulae.html" title="Class encompassing a list of `OrClause` linked by and operators.">SATFormulae</a> cnf = <a class="code" href="classSATFormulae.html" title="Class encompassing a list of `OrClause` linked by and operators.">SATFormulae</a>();
<a name="l00330"></a>00330 
<a name="l00331"></a>00331         this-&gt;sat_new_pigreek.clone(&amp;cnf);
<a name="l00332"></a>00332         <span class="keywordflow">do</span>
<a name="l00333"></a>00333         {
<a name="l00334"></a>00334                 <a class="code" href="classLabelling.html" title="Class representing a single labelling assignment.">Labelling</a> prefcand = <a class="code" href="classLabelling.html" title="Class representing a single labelling assignment.">Labelling</a>();
<a name="l00335"></a>00335                 <a class="code" href="classSATFormulae.html" title="Class encompassing a list of `OrClause` linked by and operators.">SATFormulae</a> cnfdf = <a class="code" href="classSATFormulae.html" title="Class encompassing a list of `OrClause` linked by and operators.">SATFormulae</a>();
<a name="l00336"></a>00336                 cnf.<a class="code" href="classSATFormulae.html#a613cef1d45631a255b65718f51c5024c" title="Method for cloning (not coping the pointers) this object into a new one.">clone</a>(&amp;cnfdf);
<a name="l00337"></a>00337 
<a name="l00338"></a>00338                 <span class="keywordflow">while</span> (<span class="keyword">true</span>)
<a name="l00339"></a>00339                 {
<a name="l00340"></a>00340                         <a class="code" href="classLabelling.html" title="Class representing a single labelling assignment.">Labelling</a> res = <a class="code" href="classLabelling.html" title="Class representing a single labelling assignment.">Labelling</a>();
<a name="l00341"></a>00341                         <span class="keywordflow">if</span> (!this-&gt;satlab(cnfdf, &amp;res))
<a name="l00342"></a>00342                         {
<a name="l00343"></a>00343                                 <span class="keywordflow">break</span>;
<a name="l00344"></a>00344                         }
<a name="l00345"></a>00345 
<a name="l00346"></a>00346                         <span class="keywordflow">if</span> (debug)
<a name="l00347"></a>00347                         {
<a name="l00348"></a>00348                                 cout &lt;&lt; endl;
<a name="l00349"></a>00349                                 cout &lt;&lt; <span class="stringliteral">&quot;{&quot;</span>;
<a name="l00350"></a>00350                                 <a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> it;
<a name="l00351"></a>00351                                 <span class="keywordflow">for</span> (it = res.<a class="code" href="classLabelling.html#af8aa0d976a665c1a9ebbdb801d0a867d" title="Returns the set of arguments labelled as `in`.">inargs</a>()-&gt;<a class="code" href="classSetArguments.html#aaee058feaed861edf27739fa04f374ef" title="Begin of the iterator for this set of arguments.">begin</a>(); it != res.<a class="code" href="classLabelling.html#af8aa0d976a665c1a9ebbdb801d0a867d" title="Returns the set of arguments labelled as `in`.">inargs</a>()-&gt;<a class="code" href="classSetArguments.html#a551272d71c803f64efc155b04f41e775" title="End of the iterator for this set of arguments.">end</a>();
<a name="l00352"></a>00352                                                 it++)
<a name="l00353"></a>00353                                 {
<a name="l00354"></a>00354                                         cout &lt;&lt; (*it)-&gt;<a class="code" href="classArgument.html#a95323c2bfcbb4c0d494acc13f76cc28a" title="Method returning the name of the argument.">getName</a>() &lt;&lt; <span class="stringliteral">&quot; &quot;</span>;
<a name="l00355"></a>00355                                 }
<a name="l00356"></a>00356                                 cout &lt;&lt; <span class="stringliteral">&quot;}&quot;</span> &lt;&lt; endl;
<a name="l00357"></a>00357                         }
<a name="l00358"></a>00358 
<a name="l00359"></a>00359                         res.<a class="code" href="classLabelling.html#a600661b61ebd7f0da5faea3fdef97b6c" title="Clone this labelling into a new one.">clone</a>(&amp;prefcand);
<a name="l00360"></a>00360                         <span class="keywordflow">if</span> (res.<a class="code" href="classLabelling.html#af8aa0d976a665c1a9ebbdb801d0a867d" title="Returns the set of arguments labelled as `in`.">inargs</a>()-&gt;<a class="code" href="classSetArguments.html#a66d5b1cc6b684700c2394a8cf62ef7f0" title="Retuns the cardinality of this set.">cardinality</a>() == C-&gt;cardinality())
<a name="l00361"></a>00361                                 <span class="keywordflow">break</span>;
<a name="l00362"></a>00362 
<a name="l00363"></a>00363                         <a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> iter;
<a name="l00364"></a>00364                         <span class="keywordflow">for</span> (iter = res.<a class="code" href="classLabelling.html#af8aa0d976a665c1a9ebbdb801d0a867d" title="Returns the set of arguments labelled as `in`.">inargs</a>()-&gt;<a class="code" href="classSetArguments.html#aaee058feaed861edf27739fa04f374ef" title="Begin of the iterator for this set of arguments.">begin</a>(); iter != res.<a class="code" href="classLabelling.html#af8aa0d976a665c1a9ebbdb801d0a867d" title="Returns the set of arguments labelled as `in`.">inargs</a>()-&gt;<a class="code" href="classSetArguments.html#a551272d71c803f64efc155b04f41e775" title="End of the iterator for this set of arguments.">end</a>();
<a name="l00365"></a>00365                                         iter++)
<a name="l00366"></a>00366                         {
<a name="l00367"></a>00367                                 cnfdf.<a class="code" href="classSATFormulae.html#a24f192aef15c7338da94440fbf11a1fd" title="Method for appending a new OrClause to the other clause.">appendOrClause</a>(<a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>(1, (*iter)-&gt;InVar()));
<a name="l00368"></a>00368                         }
<a name="l00369"></a>00369 
<a name="l00370"></a>00370                         <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a> difference = <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a>();
<a name="l00371"></a>00371                         this-&gt;C-&gt;setminus(res.<a class="code" href="classLabelling.html#af8aa0d976a665c1a9ebbdb801d0a867d" title="Returns the set of arguments labelled as `in`.">inargs</a>(), &amp;difference);
<a name="l00372"></a>00372                         <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a> remaining = <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>();
<a name="l00373"></a>00373                         <span class="keywordflow">for</span> (iter = difference.<a class="code" href="classSetArguments.html#aaee058feaed861edf27739fa04f374ef" title="Begin of the iterator for this set of arguments.">begin</a>(); iter != difference.<a class="code" href="classSetArguments.html#a551272d71c803f64efc155b04f41e775" title="End of the iterator for this set of arguments.">end</a>(); iter++)
<a name="l00374"></a>00374                         {
<a name="l00375"></a>00375                                 remaining.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*iter)-&gt;InVar());
<a name="l00376"></a>00376                         }
<a name="l00377"></a>00377                         cnfdf.<a class="code" href="classSATFormulae.html#a24f192aef15c7338da94440fbf11a1fd" title="Method for appending a new OrClause to the other clause.">appendOrClause</a>(remaining);
<a name="l00378"></a>00378                 }
<a name="l00379"></a>00379 
<a name="l00380"></a>00380                 <span class="keywordflow">if</span> (prefcand.<a class="code" href="classLabelling.html#ac717b73662047c2ab68e0828ff3dc54e" title="Check whether or not this labelling is empty.">empty</a>())
<a name="l00381"></a>00381                         <span class="keywordflow">break</span>;
<a name="l00382"></a>00382 
<a name="l00383"></a>00383                 this-&gt;labellings.push_back(prefcand);
<a name="l00384"></a>00384 
<a name="l00385"></a>00385                 <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a> oppsolution = <a class="code" href="classOrClause.html" title="Class encompassing a list of SAT variables (type `Variable`) linked by or operators.">OrClause</a>();
<a name="l00386"></a>00386                 <a class="code" href="classSetArgumentsIterator.html" title="Class defining a const iterator for the elements of a set of arguments.">SetArgumentsIterator</a> it;
<a name="l00387"></a>00387 
<a name="l00388"></a>00388                 <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a> difference = <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a>();
<a name="l00389"></a>00389                 this-&gt;C-&gt;setminus(prefcand.<a class="code" href="classLabelling.html#af8aa0d976a665c1a9ebbdb801d0a867d" title="Returns the set of arguments labelled as `in`.">inargs</a>(), &amp;difference);
<a name="l00390"></a>00390                 <span class="keywordflow">for</span> (it = difference.<a class="code" href="classSetArguments.html#aaee058feaed861edf27739fa04f374ef" title="Begin of the iterator for this set of arguments.">begin</a>(); it != difference.<a class="code" href="classSetArguments.html#a551272d71c803f64efc155b04f41e775" title="End of the iterator for this set of arguments.">end</a>(); it++)
<a name="l00391"></a>00391                 {
<a name="l00392"></a>00392                         oppsolution.<a class="code" href="classOrClause.html#a09a95fb8ce2a1d10ae7c22295265725c" title="Method for adding a variable at the end of the clause.">appendVariable</a>((*it)-&gt;InVar());
<a name="l00393"></a>00393                 }
<a name="l00394"></a>00394                 cnf.<a class="code" href="classSATFormulae.html#a24f192aef15c7338da94440fbf11a1fd" title="Method for appending a new OrClause to the other clause.">appendOrClause</a>(oppsolution);
<a name="l00395"></a>00395 
<a name="l00396"></a>00396         } <span class="keywordflow">while</span> (<span class="keyword">true</span>);
<a name="l00397"></a>00397 
<a name="l00398"></a>00398         <span class="keywordflow">if</span> (this-&gt;labellings.empty())
<a name="l00399"></a>00399         {
<a name="l00400"></a>00400                 this-&gt;labellings.push_back(<a class="code" href="classLabelling.html" title="Class representing a single labelling assignment.">Labelling</a>());
<a name="l00401"></a>00401         }
<a name="l00402"></a>00402 }
<a name="l00403"></a>00403 
<a name="l00410"></a>00410 Preferred::Preferred(){
<a name="l00411"></a>00411         this-&gt;encoding = 0;
<a name="l00412"></a>00412         this-&gt;labellings = vector&lt;Labelling&gt;();
<a name="l00413"></a>00413         this-&gt;sat_new_pigreek = <a class="code" href="classSATFormulae.html" title="Class encompassing a list of `OrClause` linked by and operators.">SATFormulae</a>();
<a name="l00414"></a>00414 }
<a name="l00415"></a>00415 
<a name="l00416"></a>00416 Preferred::~Preferred(){
<a name="l00417"></a>00417         <span class="comment">//TODO capire se questo provoca delle memory leak!</span>
<a name="l00418"></a>00418 }
<a name="l00419"></a>00419 
<a name="l00420"></a>00420 <span class="comment">//FIXME ho modificato il prototipo di end aggiungendo un const finale! Parlarne con la Zanella!</span>
<a name="l00421"></a>00421 <span class="comment">//questa modifica serve solo per far funzionare l&#39;operatore &lt;&lt;</span>
<a name="l00441"></a>00441 <span class="comment"></span>PreferredIterator Preferred::begin()<span class="keyword"> const</span>{
<a name="l00442"></a>00442         <span class="keywordflow">return</span> PreferredIterator(this-&gt;labellings.begin());
<a name="l00443"></a>00443 }
<a name="l00444"></a>00444 
<a name="l00445"></a>00445 <span class="comment">//FIXME ho modificato il prototipo di end aggiungendo un const finale! Parlarne con la Zanella!</span>
<a name="l00446"></a>00446 <span class="comment">//questa modifica serve solo per far funzionare l&#39;operatore &lt;&lt;</span>
<a name="l00461"></a>00461 <span class="comment"></span>PreferredIterator Preferred::end()<span class="keyword"> const</span>{
<a name="l00462"></a>00462         <span class="keywordflow">return</span> PreferredIterator(this-&gt;labellings.end());
<a name="l00463"></a>00463 }
<a name="l00464"></a>00464 
<a name="l00469"></a>00469 <a class="code" href="classSetArgumentsVector.html" title="Class representing a vector of labelling assignment.">SetArgumentsVector</a>* Preferred::getSolution(){
<a name="l00470"></a>00470         <a class="code" href="classSetArgumentsVector.html" title="Class representing a vector of labelling assignment.">SetArgumentsVector</a>* result=<span class="keyword">new</span> <a class="code" href="classSetArgumentsVector.html" title="Class representing a vector of labelling assignment.">SetArgumentsVector</a>();
<a name="l00471"></a>00471         <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a>* cloned;
<a name="l00472"></a>00472         <span class="keywordflow">for</span> (<span class="keyword">auto</span> it=this-&gt;labellings.begin(); it!=this-&gt;labellings.end();it++){
<a name="l00473"></a>00473                 cloned=<span class="keyword">new</span> <a class="code" href="classSetArguments.html" title="Class encompassing a set of arguments.">SetArguments</a>();
<a name="l00474"></a>00474                 (*it).inargs()-&gt;clone(cloned);
<a name="l00475"></a>00475                 result-&gt;<a class="code" href="classSetArgumentsVector.html#ae6509c9af6ffd7d9bbee2e0fbe3691ec" title="add a new SetArguments in this set">push_back</a>(cloned);
<a name="l00476"></a>00476         }
<a name="l00477"></a>00477         <span class="keywordflow">return</span> result;
<a name="l00478"></a>00478 }
<a name="l00479"></a>00479 
<a name="l00480"></a>00480 
<a name="l00488"></a><a class="code" href="Preferred_8h.html#aa20dbcd7a3fec439ee99c7473411aad9">00488</a> ostream&amp; <a class="code" href="Argument_8cpp.html#a76ef732a0021f3ac6698582cf94a079e">operator&lt;&lt;</a>(ostream&amp; stream, <span class="keyword">const</span> Preferred&amp; pref){
<a name="l00489"></a>00489         stream &lt;&lt; <span class="stringliteral">&quot;{ &quot;</span>;
<a name="l00490"></a>00490         <span class="keywordflow">for</span> (PreferredIterator it=pref.begin(); it!=pref.end();it++){
<a name="l00491"></a>00491                 stream &lt;&lt; <span class="stringliteral">&quot;{ &quot;</span>;
<a name="l00492"></a>00492                 <span class="keywordflow">for</span> (<span class="keyword">auto</span> itarg=(*it).inargs()-&gt;begin();itarg!=(*it).inargs()-&gt;end();itarg++){
<a name="l00493"></a>00493                         stream &lt;&lt; (*itarg)-&gt;getName() &lt;&lt; <span class="stringliteral">&quot; &quot;</span>;
<a name="l00494"></a>00494                 }
<a name="l00495"></a>00495                 stream &lt;&lt; <span class="stringliteral">&quot;} &quot;</span>;
<a name="l00496"></a>00496         }
<a name="l00497"></a>00497         stream &lt;&lt; <span class="stringliteral">&quot;}&quot;</span>;
<a name="l00498"></a>00498         <span class="keywordflow">return</span> stream;
<a name="l00499"></a>00499 }
</pre></div></div><!-- contents -->
</div>
  <div id="nav-path" class="navpath">
    <ul>
      <li class="navelem"><b>Preferred.cpp</b>      </li>

    <li class="footer">Generated on Fri Jan 17 2014 11:47:51 for SemOpt by
    <a href="http://www.doxygen.org/index.html">
    <img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.6.1 </li>
   </ul>
 </div>


</body>
</html>
